FDL - Step of Proof: can-apply-p-co-restrict

Step of Proof: can-apply-p-co-restrict

Inference at *
Iof proof for Lemma can-apply-p-co-restrict:

A, B:Type, f:(A

(B + Top)), P:(A

), p:(

x:A. Dec(P(x))), x:A.

(

can-apply(p-co-restrict(f;p);x))

((

can-apply(f;x)) & (

P(x)))

by ((((UnivCD )
CollapseTHENA (Auto

))

)
CollapseTHEN (((Unfold `p-co-restrict` 0)

CoCollapseTHEN (((((RWO "can-apply-compose-iff" 0)
THEN (MaAuto

))

)
CollapseTHEN (((((
CoAll (RWO "do-apply-p-co-filter"))
CollapseTHEN (Auto

))

)
CollapseTHEN (((
CoAll (RWO "can-apply-p-co-filter"))
CollapseTHEN (Auto

))

))

))

))

))

Co.

Definitions p-co-restrict(f;p), f o g , x.A(x), x:A.B(x), s = t, inr x , inl x , suptype(S; T), S T, A c B, case b of inl(x) => s(x) | inr(y) => t(y), tt, ff, Unit, if b then t else f fi , Dec(P), A, False, Void, P Q, P & Q, x:A B(x), b, , can-apply(f;x), do-apply(f;x), p-co-filter(f), left + right, Top, T, x(s), f(a), x. t(x), P Q, P Q, x:AB(x), True, t T, x:A. B(x), , Type

Lemmas decidable wf, iff functionality wrt iff, can-apply-compose-iff, p-compose wf, false wf, not wf, p-co-filter wf, do-apply wf, btrue wf, bfalse wf, bool wf, squash wf, true wf, top wf, can-apply-p-co-filter, assert wf, can-apply wf, do-apply-p-co-filter